\section{Zero Footprint Runtime}\label{sec:zfp-rts}
To allow a small TCB for the kernel and subjects, a special stripped-down
version of an Ada runtime\index{runtime} is provided by the Muen project. This
runtime system (RTS\index{RTS}) contains the minimal number of packages
required to compile Ada code for Muen. An Ada runtime system with such a lean
"footprint" is called \emph{Zero Footprint Runtime} (ZFP\index{ZFP}). The
following is a list of currently supported functions and packages:

\begin{itemize}
	\item function \texttt{Ada.Unchecked\_Conversion}
	\item package \texttt{Interfaces}
	\item package \texttt{System}
	\item package \texttt{System.Machine\_Code}
	\item package \texttt{System.Storage\_Elements}
\end{itemize}

These files have been extracted from the latest sources of the GNU Compiler
Collection (GCC\index{GCC}) \cite{gcc} and are linked into a static library.
The runtime is then used to compile the Muen kernel and all native subjects
running on the kernel.

Since the ZFP runtime provides only a very limited set of Ada language features,
code using this runtime must be also very simple. Simple code is an important
pre-condition for formal verification.

The compliance of the Muen kernel to the SPARK\index{SPARK} language rules
already assures that no complex Ada features are used. Additional restriction
pragmas\index{pragma} confine the language subset even further. The currently
used restrictions are shown in listing \ref{lst:pragmas}.

\lstinputlisting[
	language=Ada,
	label=lst:pragmas,
	caption=Restriction pragmas]
	{files/restrictions.adc}

Details about restriction pragmas and their impact on the allowed Ada language
subset can be found in the GNAT Reference Manual, section 4 "Standard and
Implementation Defined Restrictions" \cite{GNAT:manual}.
